Nuprl Definition : eqv_mod_subset
13,42
postcript
pdf
a
b
(mod
s
in
g
) ==
s
(
a
* (~(
b
)))
latex
clarification:
a
b
(mod
s
in
g
) ==
s
(
a
(*
g
) ((~
g
)(
b
)))
latex
Up
groups
1
Wellformedness Lemmas
eqv
mod
subset
wf
Definitions
x
f
y
,
*
,
~
origin
b (mod s in g) == s(a * (~(b)))
b (mod s in g) == s(a (*g) ((~g)(b))) b (mod s in g) == s(a * (~(b)))
b (mod s in g) == s(a (*g) ((~g)(b)))